// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==

using DySy.Engine;
using Microsoft.ExtendedReflection.ComponentModel;
using Microsoft.ExtendedReflection.Metadata.Names;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.Pex.Engine.Packages;
using Microsoft.Pex.Framework.ComponentModel;

namespace DySy.Framework
{
    public sealed class DySyAnalysisAttribute
        : PexComponentElementDecoratorAttributeBase
        , IPexExplorationPackage, IPexPathPackage
        , IDySyOptions
    {
        int _maxStackDepth = 32;
        bool _compact, _arrays;

        #region IDySyOptions Members
        /// <summary>
        /// up to which stack depth to track conditions
        /// </summary>
        public int MaxStackDepth
        {
            get { return this._maxStackDepth; }
            set { this._maxStackDepth = value; }
        }

        /// <summary>
        /// whether a compact (but potentially less readable) presentation of the inferred conditions should be shown
        /// </summary>
        public bool Compact
        {
            get { return this._compact; }
            set { this._compact = value; }
        }

        /// <summary>
        /// whether to infer properties of array elements
        /// </summary>
        public bool Arrays
        {
            get { return this._arrays; }
            set { this._arrays = value; }
        }
        #endregion

        /// <summary>
        /// Gets the name of this package.
        /// </summary>
        /// <value>The name.</value>
        public string Name
        {
            get { return "DySy"; }
        }

        protected sealed override void Decorate(Name location, IPexDecoratedComponentElement host)
        {
            SafeDebug.AssumeNotNull(location, "location");
            SafeDebug.AssumeNotNull(host, "host");

            host.AddExplorationPackage(location, this);
            host.AddPathPackage(location, this);
        }


        #region IPexPathPackage Members
        void IPexPathPackage.Load(IContainer pathContainer)
        {
            pathContainer.AddComponent("DySyPathAnalyzer", new DySyPathAnalyzer());
        }

        object IPexPathPackage.BeforeRun(IPexPathComponent host)
        {
            return null;
        }

        /// <summary>
        /// First main entry into Dysy
        /// Collect data, one call stack height at a time
        /// </summary>
        void IPexPathPackage.AfterRun(IPexPathComponent host, object data)
        {
            DySyPathAnalyzer dySyPathAnalyzer =
                ServiceProviderHelper.GetService<DySyPathAnalyzer>(host.Site);
            dySyPathAnalyzer.Analyze();
        }
        #endregion


        #region IPexExplorationPackage Members
        void IPexExplorationPackage.Load(
            IContainer explorationContainer) {
            explorationContainer.AddComponent(
                "DySyManager", 
                new DySyManager(this));
        }

        void IPexExplorationPackage.Initialize(
            IPexExplorationEngine host) { }

        object IPexExplorationPackage.BeforeExploration(
            IPexExplorationComponent host)
        {   return null; }

        /// <summary>
        /// Second main entry into DySy
        /// Dump collected information
        /// </summary>
        void IPexExplorationPackage.AfterExploration(
            IPexExplorationComponent host, 
            object data) {
            DySyManager dySyManager =
                ServiceProviderHelper.GetService<DySyManager>(host.Site);
            dySyManager.Dump();
        }
        #endregion
    }
}